package karpiel.boguchwal.wojciech.przemek


object Ast {

  case object UnitValue extends Ast

  case object UnitType extends Ast

  case object EmptyType extends Ast

  case class EmptyElim(anyType: Ast) extends Ast

  case class Universe(i: Int) extends Ast

  case class Bruijn(i: Int, name: Option[String] = Option.empty) extends Ast {
    override def equals(o: scala.Any): Boolean = {
      o.isInstanceOf[Bruijn] && o.asInstanceOf[Bruijn].i == i
    }
  }

  case class PiType(typeT: Ast, value: Ast) extends Ast

  case class PiValue(typeT: Ast, value: Ast) extends Ast

  case class PiElim(piValue: Ast, argument: Ast) extends Ast

  case class SumType(aType: Ast, bType: Ast) extends Ast

  case class SumInl(aValue: Ast, bType: Ast) extends Ast //todo można jakos wywnioskować bType?
  case class SumInr(aType: Ast, bValue: Ast) extends Ast //todo można jakos wywnioskować aValue?
  case class SumElim(aFn: Ast, bFn: Ast) extends Ast

  case class SigmaType(pi: Ast) extends Ast

  case class SigmaValue(x: Ast, aX: Ast, xToAType: Ast) extends Ast

  case class SigmaElim(pi: Ast) extends Ast

  case class Proj1(sigma: Ast) extends Ast

  case class Proj2(sigma: Ast) extends Ast

  case class IdType(x: Ast, y: Ast) extends Ast

  case class Refl(x: Ast) extends Ast

  /**
    * @param typeFunc : Pi(x:A, Pi(y:A, Id(x,y) -> U))
    * @param reflFunc : Pi(x:A, typeFunc(x,x,Refl(x))
    */
  case class J(typeFunc: Ast, reflFunc: Ast) extends Ast //chyba w normalizacji coś jak PiElim(PiInd(C,c),c `x`, `x`, Refl(`x`)) => c(x)
  //path concatenation can be defined based on J
  case object BoolType extends Ast //theoretically equivalent to Sum(Unit,Unit)
  case object BoolTrue extends Ast //theoretically equivalent to Inl(tt,Unit)
  case object BoolFalse extends Ast //theoretically equivalent to Inr(Unit,tt)
  case class BoolElim(ifTrue: Ast, ifFalse: Ast) extends Ast

  /**
    * BoolElim to indukcja, potrzeba jeszcze rekurencji
    */
  case class BoolRec(boolToType: Ast, ifTrue: Ast, ifFalse: Ast) extends Ast

  // Nat := W(bool, b -> recBool(U0,Emplty,Unit,b))
  case class WType(arityFn: Ast) extends Ast

  /**
    * TODO jakoś zebrać wType inaczej
    *
    * @param label : A
    * @param fn    B(label)-> WxB(x))
    */
  case class WSup(wType: Ast, label: Ast, fn: Ast) extends Ast

  /**
    *
    * @param e    E: WxB(x) -> U
    * @param eSup esup:
    *             Pi(a:A,
    *             Pi (u: B(a) -> WxBx,
    *             Pi(q: Pi(y:B(a), E(u(y))),
    *             E(sup(a,u)))))))
    *             //dodatkowe info: PiElim(WElim(...),WSup(a,u)) := eSup(a,u, f o u)
    * @return ret: Pi(z:W(x)B(X)), E(z))
    */
  case class WElim(e: Ast, eSup: Ast) extends Ast

  /**
    * Should be bruinized (może się bardziej przydać jak będą moduły albo co)
    */
  case class Var(name: String) extends Ast

  case class NamedType(name: String, typeT: Ast) extends Ast

}

sealed trait Ast {
}
